﻿/************************************************************************
* AIDE - Automata Identification Engine
* Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
* **********************************************************************
* This program is free software; you can redistribute it and/or modify it
* under the terms of the GNU Lesser General Public License (LGPL) published
* by the Free Software Foundation; either version 2.1 of the License, or (at your
* option) any later version. This program is distributed without any
* warranty. See the GNU Lesser General Public License for more details.
* ***********************************************************************
* File         :     AIDE\Oracles\NFMs\Oracle_MAT_Ideal.cs
* Description  :     Implementation of Ideal Oracle  for MAT setting of Mealy machine learning
* Change log   :     -Jan 2013: Initial version
*                    -22 Feb 2013: Add Symbol T
* To Do        :
************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Utils;
using SMLib.Automata.Base;
using SMLib.Automata.MM;


namespace AIDE.Oracles.NFMs
{
	/// <summary>
	/// An ideal oracle which realy knows the machine!
	/// </summary>
	public class Oracle_MAT_Ideal : IOracle_MAT_MM
	{
		Alphabet inpAlph, outpAlph;
		public int numberOfMQ, numberOfEQ;
		MealyMachine SUT;

		public Oracle_MAT_Ideal(MealyMachine SUT)
		{
			numberOfEQ = 0;
			numberOfMQ = 0;
			this.SUT = SUT;
			inpAlph = SUT.InputAlphabet;
			outpAlph = SUT.OutputAlphabet;
		}

		public Alphabet InputAlphabet
		{
			get
			{
				return inpAlph;
			}
		}

		public Alphabet outputAlphabet
		{
			get
			{
				return outpAlph;
			}
		}


		MealyMachine.Mealy_State nextStep(MealyMachine.Mealy_State currentNode, ISymbol step, out ISymbol output)
		{
			foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
			{
				if (t.inLabel.Equals(step))
				{
					output = t.outLabel;
					return (MealyMachine.Mealy_State)t.Destination;
				}
			}
			output = null;
			return null;
		}


		/// <summary>
		/// Check Whether the an input word results to an outputword or not
		/// <remarks>[To Do: Remove this function]</remarks>
		/// </summary>
		/// <param name="input">the input word</param>
		/// <param name="output">the output word</param>
		/// <returns>true if they match, false if not</returns>
		public bool MemberQ(Word input, Word output)
		{
			numberOfMQ++;
			MealyMachine.Mealy_State currentNode = (MealyMachine.Mealy_State)SUT.InitialState;
			for (int i = 0; i < input.Length; i++)
			{
				ISymbol outputSymbol;
				currentNode = nextStep(currentNode, input.GetSymByIndex(i), out outputSymbol);

				if (!outputSymbol.Equals(output.GetSymByIndex(i)) || currentNode == null)
					return false;
			}
			return true;
		}
		/*
		IOracleLogHelper logHelper;
		*/

		public void SetLogger(IOracleLogHelper logHelper)
		{
			//this.logHelper=logHelper;
		}


		/// <summary>
		/// Examine an input word to find out its corresponding output
		/// </summary>
		/// <param name="subwords">the subwords of the input word</param>
		/// <returns>the resulting output</returns>
		public Word OutputTrace(params Word[] subwords)
		{
			numberOfMQ++;
			MealyMachine.Mealy_State currentNode = (MealyMachine.Mealy_State)SUT.InitialState;
			Word output = new Word();
			foreach (Word subword in subwords)
			{
				for (int i = 0; i < subword.Length; i++)
				{
					ISymbol outputSymbol;
					currentNode = nextStep(currentNode, subword.GetSymByIndex(i), out outputSymbol);
					output.AddSymbol(outputSymbol);
				}
			}
			return output;
		}


		public ISymbol LastOutput(Word prefix, Word suffix)
		{
			Word output = OutputTrace(prefix, suffix);
			if (output.Length > 0)
				return output.GetSymByIndex(output.Length - 1);
			else
				return null;
		}


		/// <summary>
		/// Two corresponding nodes (of two Mealy Machine), AND the word we have seen to this state.
		/// We don'anotherRow require to also store the output (because with input, we can determine output!)
		/// ** It is used in Hopcroft-Karp Algorithm (function EquivalenceQ, bellow) to compare two DFAs.
		/// </summary>
		class CorrespondingNodes
		{
			public CorrespondingNodes(MealyMachine.Mealy_State k, MealyMachine.Mealy_State v)
			{
				Key = k;
				Value = v;
				path = new Word();
			}

			public CorrespondingNodes(MealyMachine.Mealy_State k, MealyMachine.Mealy_State v, Word prevPath, ISymbol nxt_input_step)
			{
				Key = k;
				Value = v;
				path = new Word(prevPath);
				path.AddSymbol(nxt_input_step);
			}

			public MealyMachine.Mealy_State Key;
			public MealyMachine.Mealy_State Value;
			public Word path;
		}


		/// <summary>
		/// See if to DFA are equal myOracle NEG. If they are not equal, find a counterexample to show the difference
		/// <remarks>Based on Hopcroft-Karp Algorithm [A linear algorithm for testing equivalence of finite automata]</remarks>
		/// </summary>
		/// <param name="conjucture">the conjecture to be examined</param>
		/// <returns>
		/// if null, the models are the same.
		/// if not, it is a counterexample which shows the models are not the same
		/// </returns>
		public Word EquivalenceQ(MealyMachine conjucture)
		{
			numberOfEQ++;

			//System.Diagnostics.Process currentProcess = System.Diagnostics.Process.GetCurrentProcess();
			//long totalBytesOfMemoryUsed = currentProcess.WorkingSet64;

			Stack<CorrespondingNodes> st = new Stack<CorrespondingNodes>();
			//List<FlaggedList<MealyMachine.Mealy_State>> allSets = new List<FlaggedList<MealyMachine.Mealy_State>>();

			List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> > >
			allSets = new List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> > >();

			// For every state q in Q1 union Q2 , MakeSet(q)
			foreach (MealyMachine.Mealy_State n in SUT.GetStates())
			{
				ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> >
				equivalents = new ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> >();
				equivalents.Add(n);
				equivalents.value = n.ListOfAllInputOutputs();

				allSets.Add(equivalents);
			}
			foreach (MealyMachine.Mealy_State n in conjucture.GetStates())
			{
				ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> >
				equivalents = new ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> >();
				equivalents.Add(n);
				equivalents.value = n.ListOfAllInputOutputs();

				allSets.Add(equivalents);
			}

			// Union(s0_1,s0_2)
			ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols> > s1, s2;
			s1 = allSets[0];
			s2 = allSets[SUT.Size];
			s1.Union(s2);
			allSets.RemoveAt(SUT.Size);

			//Push (s0_1,s0_2) on the stack
			st.Push(new CorrespondingNodes((MealyMachine.Mealy_State)SUT[0], (MealyMachine.Mealy_State)conjucture[0]));

			//* While S is non-empty
			while (st.Count != 0)
			{
				//* Pop pair (q1; q2) from S
				CorrespondingNodes c = st.Pop();
				Word curentWord = c.path;
				//* For each a in Sigma 
				foreach (ISymbol a in inpAlph.AllSymbols())
				{
					ISymbol o1, o2;
					MealyMachine.Mealy_State nextA = nextStep(c.Key, a, out o1);
					MealyMachine.Mealy_State nextB = nextStep(c.Value, a, out o2);

					//* if the outputs are different, counterexample found!
					if (!o1.Equals(o2))
					{
						Word counterExample = new Word(curentWord);
						counterExample.AddSymbol(a);

						//Console.WriteLine("Memory used for Eq Query:", currentProcess.WorkingSet64 - totalBytesOfMemoryUsed);
						return counterExample;
					}

					//* Find the sets (equivalent classes) of two nodes
					int setOfA = -1, setOfB = -1;
					for (int i = 0; i < allSets.Count; i++)
					{
						if (setOfA < 0 && allSets[i].Contains(nextA))
							setOfA = i;

						if (setOfB < 0 && allSets[i].Contains(nextB))
							setOfB = i;

						if (setOfA > -1 && setOfB > -1) break;
					}


					//* if r1<>r2
					if (setOfA != setOfB)
					{
						//* if outgoings of two sets are different, counterexample found!
						//* First case: might happen for incomplete/nondeterministic mealy machine
						if (allSets[setOfA].value.Count > allSets[setOfA].value.Count)
						{
							foreach (PairOfSymbols ps in allSets[setOfA].value)
							{
								//* Counterexample found!
								if (!allSets[setOfB].value.Contains(ps))
								{
									Word counterExample = new Word(curentWord);
									counterExample.AddSymbol(a);
									counterExample.AddSymbol(ps.Input);

									//Console.WriteLine("Memory used for Eq Query:", currentProcess.WorkingSet64 - totalBytesOfMemoryUsed);
									return counterExample;
								}
							}
						}
						else //* <=
						{
							foreach (PairOfSymbols ps in allSets[setOfB].value)
							{
								//* Counterexample found!
								if (!allSets[setOfA].value.Contains(ps))
								{
									Word counterExample = new Word(curentWord);
									counterExample.AddSymbol(a);
									counterExample.AddSymbol(ps.Input);

									//Console.WriteLine("Memory used for Eq Query:", currentProcess.WorkingSet64 - totalBytesOfMemoryUsed);
									return counterExample;
								}
							}
						}

						//if (allSets[setOfA].flag == allSets[setOfB].flag)
						allSets[setOfA].Union(allSets[setOfB]);

						allSets.RemoveAt(setOfB);
						CorrespondingNodes ns = new CorrespondingNodes(nextA, nextB);
						ns.path = new Word(curentWord);
						ns.path.AddSymbol(a);
						st.Push(ns);
					}
				}
			}
			//Console.WriteLine("Memory used for Eq Query:", currentProcess.WorkingSet64 - totalBytesOfMemoryUsed);
			return null;
		}
	}
}
